Audit the Erdős 625 manuscript line by line and theorem by theorem - #52

Purpose

This is the clean literal source-audit PR stacked directly on PR #49. It reviews the canonical 625/arxiv/main.tex statement by statement and proof transition by proof transition. The canonical TeX remains frozen.

Main verdict

The audit finds one independent submission-blocking chain:

Lemma 8.3
  -> Proposition 9.2
  -> Theorem 1.

No second unrelated fatal gap was found. Sections 2–7 and Lemmas 10.1–10.2 are structurally coherent. Lemmas 8.1–8.2 are coherent and have cleaner checked replacements. Lemma 9.1 is superseded by the matching-restriction/q-only route and is not an independent bottleneck.

The precise unresolved theorem is the exact aggregate reindexing of attained physical high skeletons by:

block-level matching support
+ one admissible deficit per selected cell
+ local partial physical matching fibres,

with pointwise preservation of the bare aggregate weight.

Audit artifacts

• 625/audits/LINE_BY_LINE_THEOREM_AUDIT_2026-07-27.md
• 625/audits/THEOREM_STATUS_MANIFEST_2026-07-27.json
• 625/experiments/extract_line_by_line_audit_map.py
• 625/experiments/check_line_by_line_audit.py

The Markdown audit covers all 3159 source lines by exact ranges. Every boxed theorem, lemma, and proposition receives:

1. exact statement and proof lines;
2. dependency contract;
3. line-range proof decomposition;
4. hidden uniformity, feasibility, positivity, and rounding conditions;
5. first downstream use;
6. verdict and exact repair.

The mechanical source map records:

canonical lines: 3159
boxed statements: 14
tagged displays: 177
duplicate labels: none
duplicate equation tags: none
references to missing labels: none

Boxed-statement classifications

GREEN
  Lemma 2.1
  Lemma 6.1
  Lemma 6.2
  Lemma 10.1
  Lemma 10.2

GREEN-REWRITE
  Lemma 3.1
  Lemma 5.1
  Lemma 7.1
  Lemma 8.1
  Lemma 8.2

SUPERSEDED
  Lemma 9.1

RED
  Lemma 8.3
  Proposition 9.2
  Theorem 1

Theorem 1 and Proposition 9.2 are RED only through Lemma 8.3; their final logical deductions are valid.

Literal source ranges

Theorem 1       statement 119–130; final proof 3078–3111
Lemma 2.1       statement 295–322; proof 324–437
Lemma 3.1       statement 495–561; proof 563–740
Lemma 5.1       statement 860–869; proof 871–1121
Lemma 6.1       statement 1354–1383; proof 1385–1428
Lemma 6.2       statement 1445–1482; proof 1484–1523
Lemma 7.1       statement 1651–1659; proof 1667–1935
Lemma 8.1       statement 2053–2079; proof 2081–2146
Lemma 8.2       statement 2151–2169; proof 2171–2228
Lemma 8.3       statement 2233–2243; proof 2245–2490
Lemma 9.1       statement 2550–2565; proof 2567–2827
Proposition 9.2 statement 2832–2842; proof 2844–2865
Lemma 10.1      statement 2903–2912; proof 2914–2963
Lemma 10.2      statement 2968–2989; proof 2991–3046

Main improvements recorded

• fix equation (7.2): 2^\ell_\bullet must be 2^{\ell_\bullet};
• replace the central-range decimal checks by the exact rational certificate;
• split Lemma 3.1 into finite duality, compact-uniform convergence, root location, and derivative results;
• replace Lemma 8.1 by the square-free checked transport theorem;
• replace Lemma 8.2 by termwise square-free AM–GM;
• replace all of Lemma 8.3 by the exact aggregate physical-fibre/all-deficit route;
• replace Lemma 9.1 by direct matching restriction and one total-q estimate;
• after closure, promote the phase-resolved /8 theorem and the stronger uniform coefficient

  (ln 2)^2/8 * ln(1000/639).
  

Exact Lemma 8.3 diagnosis

The local formula (8.21) and the single global falling-factorial comparison (8.22) are correct. The unresolved step is the transition to (8.25a)–(8.26): the sentence asserting that one may complete cells, distinguish physical cells, and then forget the distinctions does not prove the required global weight-preserving fibre decomposition. A partial physical matching generally has many full completions.

The replacement theorem must prove:

attained high demand
  <-> block matching support
      + admissible deficits
      + local partial physical matching fibres,

followed by the exact aggregate weight identity and one global (n-J)_H <= n^H loss.

The checked sharper arithmetic

h * floor((3m-1)/4)
  <= h*m - h*(h+1)/2

then gives a direct all-deficit exponent

O(sqrt(n) * (log n)^(3/2)),

or O((log n)^4) with the optional first-term/tail split.

Validation

On head

619f4ccfc51ae9a28bb3924d7e894ed18d742059

the dedicated workflow run 30248592892 passed all jobs:

• literal line-by-line audit checker under ordinary Python;
• the same checker under python -O;
• exact theorem/proof-range and source-blob validation;
• exact boxed RED-chain validation;
• generated source-map artifact upload;
• Section VIII exact regression under ordinary and optimized Python;
• reader-facing TeX checks;
• focused Lean 4.31 warning-fatal builds of the sharp all-deficit interfaces;
• placeholder and project-axiom rejection.

The generated source-map artifact and checker log are attached to the successful workflow run.

Scope boundary

This PR is an audit, not a proof closure. It does not prove the outstanding pointwise aggregate-weight identity, the final bare-skeleton estimate, Proposition 9.2, or Erdos625Statement. The abstract and Theorem 1 must remain conditional until the twelve acceptance gates listed in the audit are green on one integrated commit.